body {
    font-family: Times; 
    color: black;
    background-color: #f2f7ea;
    background-image: url(../img_original/background.png);
    background-position: top left;
    background-attachment: fixed;
    background-repeat: no-repeat;
}

/* see JavascriptConsole.js: px written there, too */
div.header {
 margin-left: 90px;
 margin-right: 4%;
 height: 40px;
 align: center
}

div.headerform {
 margin-left: 40%;
 align: center
}

/* see JavascriptConsole.js: px written there, too */
div.content {
 margin-top: 0em;
 margin-left: 90px;
 margin-right: 4%;
}

div.navbar {
   align:center
}

/* position: absolute; top: 100px; height: 400px; */

@media screen {  /* hide from IE3 */
a[href]:hover { background: #ffa }
}

DIV.subtoc {
	   padding: 1em; 
	   border: solid thin; 
	   margin: 1em 0;
	   line-height: 140%;
	   background: #ddd
	   }

.changed {
background-color: #e5bbbb; 
}

a.link {
 color: #00f;
 text-decoration: underline
}

a.solution {
 cursor: pointer;
 color: #080;
}

a.link:hover {
    cursor:pointer;
}

h1,h2,h3,h4,h5,h6 {
   margin-top: .8em;
   margin-bottom: .5em;
}

.partheading {
   font-size: 70%;
}

.chapterheading {
   font-size: 70%;
}

ol {
   list-style-type: decimal;
}

ol.exercise { 
	  border: none; 
	    list-style-type: lower-alpha; 
	    }

ol ol {
   list-style-type: lower-alpha;
}

ol ol ol {
   list-style-type: lower-roman;
}

ol ol ol ol {
   list-style-type: upper-alpha;
}

.normaltext {
  line-height: 140%;
  text-align: justify;
  padding-bottom: 8pt;
}

.exercise {
  	  line-height: 140%;
	  text-align: justify;
	  padding-bottom: 8pt;
	  padding: 1em; 
	  border: solid thin; 
	  border-color: #999;
	  margin: 1em 0;
	  line-height: 140%;
	  background: #fff
}

.footnote {
  text-align: justify;
  font-size: 0.75em;
}

.epigraph {
   text-align: justify;
  line-height: 120%;
   font-size: 85%; 
  padding-bottom: 8pt;
} 

.meta {
   text-align: center;
   font-size: 75%; 
   color: gray;
} 

.footnote {
   font-size: 75%; 
} 

.footnote p { margin: 0; text-indent:1.5em; }

.figure {
 align: center;
 background-color: lavender;
}

.table {
background-color: pink;
}



.navigation {
   color: red;
   text-align: right;
   font-style: italic;
}

img.link:hover {
    cursor:pointer;
    background: #7777ff none; 
}
      
img.link {
    padding:2px;
}

form.code {
    margin-top: 5;
    margin-bottom: 7;
}

td.code {
    border-width: 2;
}

.smallprint {
   color: gray;
   font-size: 75%;
   text-align: right;
}

.smallprint hr {
   text-align: left;
   width: 40%;
}

.disable {
   /* color: #e5e5e5; */
color: gray;
}

div.popup {
     font-family: Times; 
      color: #777;
      background-color: rgba(255,255,255,1); /* last item was 0.6 */
      cursor: move;
      width: auto;
      height: auto;
}

div.popupinner {
       margin-top: 20px;
       margin-bottom: 20px;
       margin-left: 20px;
       margin-right: 20px;
}

div.popup:hover {
      cursor: move;
      background-color: rgba(255,255,255,1);
}

input.popupbutton {
     font-family: Times; 
     font-size: 90%;
	     cursor: pointer; 
	     color: #444;
	     background-color: rgba(255,255,255,0.4);
}

input.popupbutton:hover {
    cursor: pointer; 
      background-color: rgba(255,255,255,1);
}

img.popupinput {
     font-family: monospace; 
      color: black;
      background-color: rgba(200,200,255,0.8);
}

img.popupinput:hover {
      background-color: rgba(200,200,255,1);
}

textarea.popupoutput {
     font-family: monospace; 
      color: black;
      background-color: rgba(200,200,200,0.8);
}

/* blockquote from http://www.cs.tut.fi/~jkorpela/html/bq.html */
blockquote { border : solid thin; border-color: #999; padding : 3px; 
   margin-left: 3em; margin-top:0.5em; margin-bottom:0.5em;
   background: #f9f9f9 none; color: #000; }
.credit { text-align : right; page-break-before: avoid;
   font-family:Verdana,Arial,Helvetica,sans-serif; }
.credit small { font-size: 80%; } 
blockquote p { margin: 0; text-indent:1.5em; }
blockquote pre { margin: 0; }

pre.jush-js {     
   cursor: pointer; 
   border : solid thin; 
   border-width: 2px;
   border-color: #999; 
   background-color: rgba(220,220,255,1);
   padding:4px;
}

pre.jush-js:hover {     
   cursor: pointer; 
   border : 'solid thick'; 
   border-color: #77f; 
}

span.schemeinline { font-family: monospace }

span.javascriptinline { font-family: monospace }

span.javascriptinlinechanged { 
   font-family: monospace;
   color: #900;
}
